ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), v:ecl-trans-tuple{i:l}(ds; da),
L:(event-info(ds;da) List). ecl-trans-state(v; L)  ecl-trans-type(v) 

latex

Definitions	Id, t  T, x. t(x), x:A. B(x), fpf(A; a.B(a)), Knd, ecl-trans-tuple{i:l}(ds; da), event-info(ds;da), ecl-trans-init(v), ecl-trans-state-from(v; z; L), ecl-trans-state(v; L)
Lemmas	ecl-trans-state-from wf, ecl-trans-init wf, event-info wf, ecl-trans-tuple wf, Knd wf, fpf wf, Id wf